ds:fpf(Id; x.Type), knd:Knd, T:Type, l:IdLnk, dt:fpf(Id; x.Type), g:((tg:Id
ds:fpf(Id; x.Type), knd:Knd, T:Type, l:IdLnk, dt:fpf(Id; x.Type), g:( (decl-state(ds)T
ds:fpf(Id; x.Type), knd:Knd, T:Type, l:IdLnk, dt:fpf(Id; x.Type), g:( (decl-type{i:l}
ds:fpf(Id; x.Type), knd:Knd, T:Type, l:IdLnk, dt:fpf(Id; x.Type), g:( (decl-type(dt; tg
ds:fpf(Id; x.Type), knd:Knd, T:Type, l:IdLnk, dt:fpf(Id; x.Type), g:( (decl-type() List))) List).
Rsends(ds; knd; T; l; dt; g)  es_realizer{i:l} 

latex

Definitions	x. t(x), Rsends(ds; knd; T; l; dt; g), es_realizer{i:l}, t  T, x:A. B(x), x(s)
Lemmas	fpf wf, Id wf, unit wf, rationals wf, bool wf, finite-prob-space wf, Knd wf, IdLnk wf, decl-type wf, decl-state wf